Nuprl Lemma : f-rel-causal
11,40
postcript
pdf
es
:ES,
L
:(Id List). fischer(
L
)
(
e1
,
e2
:E. Try(
e1
)
Try(
e2
)
e1
<f
e2
(
e1
<
e2
))
latex
Definitions
loc(
e
)
,
f-rel{$z,$wanted}(
es
;
L
;
e1
;
e2
)
,
A
c
B
,
isrcv(
e
)
,
Id
,
x
:
A
B
(
x
)
,
let
x
,
y
=
A
in
B
(
x
;
y
)
,
the rcv(wanted message from
e1
to
j
)
,
P
&
Q
,
t
...$L
,
(
e
<
e'
)
,
e
<
e'
,
e
loc
e'
,
(
e
<loc
e'
)
,
False
,
Try(
e
)
,
E
,
t
.1
,
fischer(
L
)
,
@
i
(
x
:
T
)
,
x
L
.
P
(
x
)
,
P
Q
,
(
x
l
)
,
A
,
s
=
t
,
@
e
(
x
v
)
,
type
List
,
ES
,
b
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
t
T
Lemmas
es-le
weakening
eq
,
es-le-causle
,
es-sender-causl
,
f-wanted-isrcv
,
f-wanted
wf
,
es-causle
weakening
locl
,
es-causl
transitivity2
,
es-causl
transitivity1
,
sender-f-wanted
origin
es:ES, L:(Id List). fischer(L) 
(e1, e2:E. Try(e1) Try(e2) e1 <f e2 (e1 < e2)) es:ES, L:(Id List). fischer(L) (e1, e2:E. Try(e1) Try(e2) e1 <f e2 (e1 < e2)) 
B
B(x)
loc e' 
L. P(x)
A
v)
b
B(x)